$\forall$${\it the\_es}$:ES, $j$:E. $\neg$first($j$) $\Rightarrow$ (pred($j$) $<$loc $j$)